FDL - Nuprl Lemma : chain_sys_ind

Nuprl Lemma : chain_sys_ind_wf

11,40

X:Type{j}, Cmd:Type{i}, x:chain_sys(Cmd), input:(Cmd

X), update:(Id

(Cmd List)

X).
chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from,cmds))

Definitions Type, t T, x:AB(x), s = t, Id, type List, x:A. B(x), f(a), x(s1,s2), x(s), x:A B(x), left + right, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), chain_sys(Cmd)

Lemmas member wf, chain sys wf, Id wf

Definitions	Type, t T, x:AB(x), s = t, Id, type List, x:A. B(x), f(a), x(s1,s2), x(s), x:A B(x), left + right, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), chain_sys(Cmd)
Lemmas	member wf, chain sys wf, Id wf